Tamarin Models
Below is a brief summary of the formal models used in our paper, done using the Tamarin Prover.
Mobile Visa Model – Formal model for Visa transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).
Mobile Mastercard Model – Formal model for Mastercard transactions done via payment apps, in normal as well as transport mode (both Apple Pay, Samsung Pay are modelled).
Modified Basin Visa Model – An updated model for Visa transactions done via a (plastic) card, with more details around the [IAD] and its checks; it proves that checking the format of the IAD for Visa cards would in fact detect a previous contactless limit bypass attack proposed in The EMV Standard: Break, Fix, Verify.
L1RP
Model –
Formal model proving the security of our new proposed protocol, L1RP
.